let empty : ∀(a : Type) → List a = λ(a : Type) → [] : List a in empty
